1. Field of the Invention
This invention pertains in general to hardware designs functional verification and in particular to techniques for evaluating a temporal description within a general purpose programming language.
2. Background Art
Using a temporal description to verify a hardware design is increasingly common. Hardware description languages such as the Process Specification Language (PSL) are becoming standards to verify hardware designs and various electronic design automation (EDA) tools are beginning to support the evaluation of such a temporal description. For example, a hardware description language such as System Verilog uses the temporal description mechanism to check the correctness of a hardware behavior during hardware simulation. Special purpose programming languages developed for designing hardware can adopt such a new language construct (i.e., temporal description) with an additional syntax.
Another trend of hardware design is to use a general purpose programming language such as C++ to simulate a hardware behavior. In such an environment, users use a general purpose programming language with various hardware modeling support libraries to construct a simulation model to verify hardware behaviors. Because the hardware model is written in a general purpose programming language, it is easy to mix simulation codes, which are constructed using the general purpose programming language with software.
In a general purpose programming language, however, the language syntax cannot be easily changed to support hardware simulation. It is desirable for the general purpose programming language to have a mechanism to evaluate a temporal description during hardware simulation. Moreover, it is desirable that such a mechanism be able to express a temporal description within the context of the general purpose programming language such that the temporal description is constructed with the general purpose programming language's native expression, and that variables used within the temporal description are taken from the name scope of the temporal description's location.
In addition, because the temporal logic mechanism is useful in specifying the sequence of hardware behaviors, it is desirable to use it as an ordinal expression within a general purpose programming language. In such an expression, there will be a mixture of temporal constructs and ordinal expressions. To evaluate such a mixed expression, the ordinal expression is repeatedly evaluated over the program execution. However, the ordinal execution mechanism provided by general purpose programming language compilers cannot handle such a situation.
Therefore, there is a need for a technique that effectively evaluates a temporal description within a general purpose programming language.
Additionally, temporal assertion in hardware verification uses a formal expression to describe the correct behavior of the hardware. Its formal expression is a type of regular expression to express the possible path of the sequence and/or event to occur. This formal description allows the user to express complicated hardware behavior in concise, easy to read expressions.
The formal expression contains many possible concurrent evaluation. It has a capability to describe many possible temporal sequences in one description, and the evaluation of such expression may require many concurrent operations. Thus, even if a concise expression is provided, it may not be so easy to determine if the temporal expression is really correct. Upon an unexpected failure of the evaluation, the user must determine where and how the expression led to a failure.
For debugging a hardware design in using hardware simulation, a waveform viewer is commonly used. The waveform viewer has capability of showing the timeline changes of a static location, such as for a particular signal. But the activity of evaluating a temporal assertion involves many dynamic concurrent operations and it is not possible to show such activities in prior-art waveform viewers.
Some waveform viewer has the capability to show the results of temporal evaluation in a static manner. As the nature of waveform, it is not possible to show the dynamic activities during the evaluation process.
Therefore, there is a need for methods that can effectively evaluate and dynamically displays temporal expressions.